# Script usado para reconhecer o resultado do model check

import sys
import string
import re

def getModelCheckPattern():
    return "==========================================\nreduce in (.*): modelCheck\((.*), (.*)\) .\nrewrites:.*rewrites/second\)\nresult (.*):(.*)"

def getCounterexamplePattern(qtdEstados):
    return "counterexample\(" + qtdEstados * ".*\{(.*),.*\}" + "\)"

def getCounterexampleStatesPattern(qtdEstados):
    #counterexample(nil, {P1,empty,empty,'T1} {empty,P2,    empty,'T2} {empty,empty,P3,'T3})
    return 

def getHeaderPattern():
    return "=========================================="

def getEndPattern():
    return "Bye."

def match(pattern, line):
    return re.match(pattern, line)

def contaEstadosDoCounterexample(ce):
    count = 0
    for i in ce:
        if i == "{":
            count += 1
    return count

def getMenorQtdDeEstadosNoCounterexample(ce1, ce2):
    return min(contaEstadosDoCounterexample(ce1), contaEstadosDoCounterexample(ce2))

def tratarCounterexample(ce1):
    result = ""
    for i in ce1:
        if (i == " " and (result[-1:] == " " or result[-1:] == ",")):
            None
        else:
            result += i
    return result

def eliminateMsg(state):
    result = []
    for i in state:
        if (not match("Msg", i)):
            result.append(i)
    return result

def formatState(state):
    formatedState = state
    formatedState = string.replace(formatedState, ",", " ")
    formatedState = string.replace(formatedState, "empty", "")
    formatedState = string.replace(formatedState, "none", "")
    formatedState = string.replace(formatedState, "(", "")
    formatedState = string.replace(formatedState, ")", "")
    return eliminateMsg(formatedState.split())
    #formatedState = " ".join(formatedState.split())
    #return formatedState

def getCounterexamples(states):
    result = []
    for i in states:
        temp = formatState(i)
        if (len(temp)):
            result.append(temp)
    return result

def compararCounterexamples(ce1, ce2):
    estados1 = match(getCounterexamplePattern(contaEstadosDoCounterexample(ce2)), ce2).groups()
    estados2 = match(getCounterexamplePattern(contaEstadosDoCounterexample(ce1)), ce1).groups()
    
    estados1 = getCounterexamples(estados1)
    estados2 = getCounterexamples(estados2)
    
#    print estados1
#    print estados2
    
    menor = estados1
    maior = estados2
    if (len(estados2) < len(estados1)):
        menor = estados2
        maior = estados1
    
    indice_menor = 0
    
    for indice_maior in xrange(len(maior)):
        if (menor[indice_menor] == maior[indice_maior]):
            indice_menor += 1
        if (indice_menor >= len(menor)):
            return True
    
#    for indice_maior in xrange(len(maior)):
#        if (string.strip(menor[indice_menor]) == string.strip(maior[indice_maior])):
#            indice_menor += 1
#        if (indice_menor >= len(menor)):
#            return True
    
    return False

files_name = sys.argv[1:]

if (len(files_name) != 2):
    raise "Deve-se passar exatamente 2 argumentos."

#print files_name

var_files = []
try:
    for i in files_name:
        var_files.append(open(i + ".resultado","r"))
        
except:
    for i in var_files:
        i.close()
    raise

filesModelChecks = []
for i in xrange(len(var_files)):
    modelChecks = []
    index = -1
    
    for j in var_files[i].readlines():
        if (match(getHeaderPattern(), j)):
            index += 1
            modelChecks.append("")
        if (index > -1):
            modelChecks[index] += j
            
    filesModelChecks.append(modelChecks)

#print filesModelChecks

filesProperties = []
for i in filesModelChecks:
    properties = []
    results = {}
    for j in i:
        result = match(getModelCheckPattern(), j)
        properties.append(result.groups())
    filesProperties.append(properties)


testesOk = 0
for i in xrange(len(filesProperties[0])):
    print "Checking property #" + str(i+1) + ": " + filesProperties[0][i][2]
    print "Bisimulation result:",
    if (string.strip(filesProperties[0][i][3]) == "Bool" and string.strip(filesProperties[1][i][3]) == "Bool"):
        if (string.strip(filesProperties[0][i][4]) == string.strip(filesProperties[1][i][4])):
            print "OK\n\t" + files_name[0] + ": " + string.strip(filesProperties[0][i][4])
            print "\t" + files_name[1] + ": " + string.strip(filesProperties[1][i][4])
            testesOk += 1
        else:
            print "FAIL\n\t" + files_name[0] + ": " + string.strip(filesProperties[0][i][4])
            print "\t" + files_name[1] + ": " + string.strip(filesProperties[1][i][4])
    elif (string.strip(filesProperties[0][i][3]) == "Bool" or string.strip(filesProperties[1][i][3]) == "Bool"):
        print "FAIL\n\t" + files_name[0] + ":",
        if (string.strip(filesProperties[0][i][3]) == "Bool"):
            print string.strip(filesProperties[0][i][4])
        else:
            print "counterexample"
        
        print "\t" + files_name[1] + ":",
        if (string.strip(filesProperties[1][i][3]) == "Bool"):
            print string.strip(filesProperties[1][i][4])
        else:
            print "counterexample"
    else:
        result = compararCounterexamples(tratarCounterexample(string.strip(filesProperties[0][i][4])), tratarCounterexample(string.strip(filesProperties[1][i][4])))
        if (result):
            print "OK - counterexamples are similar"
            testesOk += 1
        else:
            print "FAIL - counterexamples are not similar"
        print "\t" + files_name[0] + " - counterexample"
        print "\t" + files_name[1] + " - counterexample"

print "\nPassed in " + str(testesOk) + " properties of " + str(len(filesProperties[0]))

"""
modelChecks = []
index = -1
for i in lines:
    if (match(getHeaderPattern(), i)):
        index += 1
        modelChecks.append("")
    if (index > -1 and not match(getEndPattern(), i)):
        modelChecks[index] += i

for i in modelChecks:
    print i
"""

for i in var_files:
    i.close()
